Inference at * 2 
Iof proof for Lemma p-fun-exp-compose:



1. T : Type
2. n : 
3. 0 < n
4. h, f:(T(T + Top)). f^n - 1 o h   = primrec(n - 1;h;i,g. f o g  )
  h, f:(T(T + Top)). primrec(n;p-id();i,g. f o g  ) o h   = primrec(n;h;i,g. f o g  ) 

latex

 by (Auto THEN Subst' n = 1+(n - 1) 0 THENA Auto') 
CollapseTHEN (
CRWO "primrec_add" 0 THEN Auto THEN Reduce 0) 

latex

C1: 

C1: 5. h : T(T + Top)
C1: 6. f : T(T + Top)
C1:   primrec(1+(n - 1);p-id();i,g. f o g  ) o h   = f o primrec(n - 1;h;i,g. f o g  )  
C.

Definitions	s = t, , n+m, n - m, #$n, s ~ t, , SQType(T), {T}, P  Q, P & Q, x:A  B(x), P  Q, primrec(n;b;c), p-id(), x.A(x), f o g  , {i..j}, t  T, , {x:A| B(x)} , A  B, A, False, P  Q, Void, a < b, -n, x:A. B(x), x:AB(x), left + right, Top
Lemmas	primrec add, primrec wf, p-id wf, p-compose wf, int seg wf, le wf